Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

(co)products/(co)equalizers for Fincats and Diagrams #615

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

kris-brown
Copy link
Contributor

Main goal: implement the constructions described in Peschke and Tholen (2020) remark 2.8. This involves developing a lot of other prerequisite functionality.

Main contributions:

  • Currying FinDomFunctors into C-Set as FinDomFunctors into Set
  • pushout-based chase
    • Collage of functor
    • Conversion between C-Set and SpanC-Set (a model for C-Rel)
    • left kan extensions of FinDomFunctors into Set (or C-Set) + universal property
  • Limits/colimits the category of FinCats
  • Limits/colimits the category of Diagrams + universal properties
    • Left kan extension used to compute coequalizers for Diagram{id}

To-do:

  • Left kan extension to compute equalizers for Diagram{op}
  • Universal property of coequalizers (id) / equalizers (op).
  • Treatment of equations for (co)equalizers of FinCats

Caveats:

  • Code for (co)limits of FinCats is stored in Limits.jl to avoid circular dependency. Tests are still in test/.../FinCats.jl
  • For simplicity, FinCatPresentations are treated (but, ideally, code generically would work with FinCatGraphs as well)
  • Because of the makeshift way dynamic acsets are implemented, rather than MyCSetType() it's safer to use Base.invokelatest(MyCSetType)
  • Left kan extensions are abysmally slow (likely due to the dynamic acset hack)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant